COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BDR25\M1BDJ25\M2NGB25\M3XMAS25\M4GRK25\.
C00010 ENDMK
C⊗;
\\M0BDR25;\M1BDJ25;\M2NGB25;\M3XMAS25;\M4GRK25;\.
\F0\CABSTRACT SYNTAX AND SEMANTICS OF CONDITIONAL EXPRESSIONS


\J	Abstract syntax in general was introduced in (McCarthy 1963b, \F1Towards
a Mathematical Science of Computation\F0), and that paper should be read for
an \F1ab initio\F0 discussion of the idea.

	The abstract syntax of conditional expressions is given by four
functions and a predicate, namely:

	1. Any conditional expression \F1e\F0 satisfies iscond \F1e\F0.

	2. If \F1p\F0 is a propositional expression and \F1a\F0 and \F1b\F0
are arbitrary expressions, then mkcond(\F1p,a,b)\F0 is a conditional expressions.
Common concrete notations for it are \F2if \F1p\F2 then \F1a\F2 else \F1b\F0,
(COND \F1(p a)(T b))\F0, and \F1(p→a,b)\F0.

	3. The functions \F1s1, s2, \F0 and \F1s3\F0 extract the three parts of
the conditional expression.

	The semantics of conditional expressions are assumed well known informally.
Formally, they are given by a clause in the recursive definition of value of
expressions, namely\.

	value(\F1e,\F4x\F0) ← \F2 if\F0 ...
			...
		\F2else if \F0 iscond(\F1e) \F2 then
			(\F2if\F0 value(\F1s1(e),\F4x\F0) \F2then\F0 value(\F1s2(e),\F4x\F0)
				\F2else\F0 value(\F1s3(e),\F4x\F0))
		\F2else if\F0 ... .

\J	First order logic does not handle recursive definitions in a simple way,
so that the abstract syntax and semantics of conditional expressions have to
be described in  slightly different way.  This is done in the set of axioms
COND.AX given in the appendix to these notes in a form suitable for input to
Weyhrauch's proof checker FOL.  Along with these axioms are given a set of axioms
for equality.

	Also given is a proof as typed out by the proof checker of the sentence\.

	∀ \F1p a b c. \F0isprop(\F1p) ⊃ \F0value(mkcond(\F1p\F0,mkcond(\F1p,a,b),c))\.
\F0 = value(mkcond(\F1p,a,c\F0))).

\J	This sentence is the metamathematical equivalent of the first of the axioms
for conditional expressions given in (McCarthy 1963a, \F1A Basis for a Mathematical
Theory of Computation\F0), namely\.

	\F1(p→(p→a,b),c) = (p→a,c).

\F0\J	It is metamathematical in that the sentence refers to the values of the
expressions rather than giving an equivalence of the expressions themselves.  We
have omitted the \F4x\F0 from the \F1value\F0 function, because it would just
sit there as a constant throughout the entire proof.

	The proof is given in the output format of the proof checker which is
not the form in which the proof is written in.  The input form corresponds
closely to the reasons given after the steps.  (It would be convenient if this
correspondence were exact).  The output form omits the fetching of the axioms
sets COND.AX[257,JMC] and EQUAL.AX[257,JMC], and it also omits to mention that
\F1p,a,b, \F0and \F1c\F0 had to be "declare"ed INDVARs before the proof would
work.

	The style of the proof given is not the most natural which would be to
assume the premisses of the statement and work to the conclusions and the use
the ⊃I rule to discharge the assumptions and get implications. Instead, I
chose to first give all the instantiations of the axioms (except for one
which I forgot), the prove a lemma and give three instantiations of it, then
make all the substitutions of equals for equals that are required and finally
make the computer do all the propositional reasoning in a single application
of the \F1tautology\F0 rule.

	The proof is several times as long as it will need to be when goal
structure, simplification and a way of combining substitution and propositional
reasoning is added to the proof checker.  However it is not difficult once
you understand what you have to do, and the amount of writing the user
actually has to make takes only 10 or 15 minutes.\.


\C\F3EXERCISES\F0

	1. State and prove the metamathematical equivalent of

	\F1((p→q,r)→a,b) = (p→(q→a,b),(r→a,b))\F0.

\JIt seems to me that COND.AX and EQUAL.AX will prove adequate for this, and
the proof will be straightforward, but I haven't done the problem.  Get
FOL to accept your proof.

	2. Use the abstract syntax of conditional expressions and LISP functions
for intermediate use to give recursive functions for putting conditional
expressions in weak canonical form.  You may have to invent a minor syntactical
function or two.  Take as an argument to your function a list propositional
variables guaranteed to include all that occur in the expression.  If you feel
ambitious try the strong canonical form.

	3. Give a statement asserting that the above function does put the
expressions into canonical form.  To prove this statement will require more
machinery than has so far been introduced and might make a suitable term
project for someone.